$\forall$$T$:Type, $A$:($T$$\rightarrow\mathbb{P}$). ($\exists$$f$:detach\_fun($T$;$A$). True) $\Leftarrow\!\Rightarrow$ ($\forall$$x$:$T$. Dec($\downarrow$($A$($x$))))